e2 = first e  e1.P(e) == e1  e2  & P(e2) & e[e1,e2).P(e) 

latex

---

clarification:

es-first-since(es;e.P(e);e1;e2) == es-le(es;e1;e2) & P(e2) & alle-between1(es;e1;e2;e.P(e)) 

latex

Definitions	e2 = first e  e1.P(e), e  e' , P & Q, e[e1,e2).P(e), A
FDL editor aliases	es-first-since